package preprocessor.absorption.extended;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;

import option.KBVocabulary;

//import preprocessor.absorption.BinaryAbsorptionGuarded;

import kb.TBox;

import utils.ExecTime;
import utils.exception.AbsorptionException;
import utils.exception.CoreReasoningException;

import entities.Individual;
import entities.concept.Concept;
import entities.concept.Nominal;
import entities.concept.NotConcept;
import entities.concept.PConcept;
import entities.concept.ExistsConcept;
import entities.concept.UniversalConcept;
import entities.role.Role;

public class OptimizedUniversals extends OptimizedRestrictions{

	public static long totalUniv = 0;
	public static long rmedDefs = 0;
//	public static long repData = 0;
//	private static Set<Nominal> reps = new HashSet<Nominal>();

	public static void clearAll(){
		totalUniv = 0;
		rmedDefs = 0;
//		repData = 0;
//		reps.clear();
	}
//	public static boolean skip(Role r, Individual a, Individual b) {
//		boolean ret = false;
//		if (normalizedUniversals.containsKey(r)) {
//			Map<Concept, Set<Concept>> univ = normalizedUniversals.get(r);
//			for (Concept lhs : univ.keySet()) {
//				if (lhs.isTop() || hasRealized(lhs, a)) {
//					continue;
//				}else{
//					boolean once = true;
//					// a:A
//					for (Concept rhs : univ.get(lhs)) {
//						once &= hasRealized(rhs, b);
//						if (!once) {
//							return false;
//						}
//					}
//					ret = true;
//				}
//			}
//		}
//		return ret;
//	}
	
	//fix: for every a that has def_a removed, add a AND def_Q -> A (where a:A is in the data)
//	private static void patchNonGuardedNoms(Nominal a, PConcept defa, TBox tb) throws AbsorptionException{
//		Concept data = tb.getSpecialBinaryClass().getEntry(a, defa);
//		if(data != null && !reps.contains(a)){
//			repData++;
//			tb.getSpecialBinaryClass().addBinaryEntry(a, KBVocabulary.QUERY_GUARD, data);
//			reps.add(a);
//		}
//		return;
//	}
	
	private static void applyChanges(Nominal a, PConcept defr, Nominal b, TBox tb) 
			throws CoreReasoningException, AbsorptionException{
		PConcept defb = PConcept.newGuardPConcept(b);
		Concept entry = tb.getSpecialBinaryClass().getEntry(a, defr);
		if(entry == null){
			throw new CoreReasoningException("Error: binary entry is not in the TBox -- "+" nom: "+a+" -- defr:"+defr+" defb:"+defb);
		}
		Set<Concept> newand = new HashSet<Concept>();
		for(Concept and:Concept.reduceToConjuncts(entry)){
			if(and instanceof ExistsConcept){
				ExistsConcept ex = (ExistsConcept) and;
				Set<Concept> fs = Concept.reduceToConjuncts(ex.getFiller());
				boolean rm = fs.remove(defb);
				if(rm){
					newand.add(new ExistsConcept(ex.getRole(), Concept.getConjunctiveConcept(fs)));
					rmedDefs ++;
//					System.out.println("Removed def for "+b);
//					patchNonGuardedNoms(b, defb, tb);
				}else{
					//no change, add it back
					newand.add(and);
				}
			}else{
				newand.add(and);
			}
		}
		//update
		Concept newentry = Concept.getConjunctiveConcept(newand);
		try {
			tb.getSpecialBinaryClass().updateEntryValue(a, defr, newentry);
		} catch (AbsorptionException e) {
			e.printStackTrace();
		}

	}
	
//	//record all def_b to be removed, and do them all at once.
//	private static Map<Nominal, Map<PConcept, Set<PConcept>>> toBeRmed = new HashMap<Nominal, Map<PConcept, Set<PConcept>>>();
//	
//	private static void addToBeRmed(Nominal ln, PConcept defr, PConcept defb){
//		Map<PConcept, Set<PConcept>> im = null;
//		if (toBeRmed.containsKey(ln)) {
//			im = toBeRmed.get(ln);
//			if(im.containsKey(defr)){
//				im.get(defr).add(defb);
//			}else{
//				Set<PConcept> bs = new HashSet<PConcept>();
//				bs.add(defb);
//				im.put(defr, bs);
//				toBeRmed.put(ln, im);
//			}
//		} else {
//			im = new HashMap<PConcept, Set<PConcept>>();
//			Set<PConcept> bs = new HashSet<PConcept>();
//			bs.add(defb);
//			im.put(defr, bs);
//			toBeRmed.put(ln, im);
//		}
//	}
//	
	
	
	private static void removeDEFsDirectional(Individual lo, Individual ro, Role r, TBox tb) 
			throws CoreReasoningException, AbsorptionException{
		Nominal ln = Nominal.getNominal(lo.getName(), false);
		Nominal rn = Nominal.getNominal(ro.getName(), false);
		PConcept defr = PConcept.newGuardPConcept(r);
		applyChanges(ln, defr, rn, tb);
	}
	
	//role assertions, a set of axioms, and direction
	private static void removeDefb(Role r, Individual a, Individual b, TBox tb) 
			throws CoreReasoningException, AbsorptionException{
		if (normalizedUniversals.containsKey(r) && !tb.getRoleBox().isTransitive(r)) {
//			if(r.getRoleName().contains("isLocated")){
//				System.err.println("stop");
//			}
			boolean domainRange = false;
			Map<Concept, Set<Concept>> univ = normalizedUniversals.get(r);
			boolean fwd= true, bwd = true;
			for (Concept lhs : univ.keySet()) {
				boolean aleft = false;
				if(fwd){
					//if false, no need to do further checks
					if(lhs.isTop()){
						domainRange = true;
						fwd &= true;
					}else 
					if (isInstance(a, lhs, true, tb)) {
						aleft = true;
						fwd &= true;
					}else{
						boolean once = true;
						for (Concept rhs : univ.get(lhs)) {
							once &= isInstance(b, rhs, true, tb);
							if (!once) {
								fwd &= false;
							}
						}
						
					}
				}
				
				if(bwd){
					//check the backward direction, no need to check if backward is already falsied by other axioms
					if(domainRange){
						//for domain/range axiom, the backward direction always fails.
						bwd &= false;
					}else
					if (!aleft && isInstance(a, new NotConcept(lhs), true, tb)) {
//						System.err.println("saved");
						bwd &= true;
					}else{
						boolean once = true;
						for (Concept rhs : univ.get(lhs)) {
							once &= isInstance(b, new NotConcept(rhs) , true, tb);
							if (!once) {
								bwd &= false;
							}
						}
						
					}
				}
				
				if(!fwd && !bwd){
					return;
				}
			}
			//we can remove the proper direction of DEFb
			if(fwd) removeDEFsDirectional(a, b, r, tb);
			if(bwd) removeDEFsDirectional(b, a, tb.getRoleBox().getInverseRole(r), tb);
		}
		
	}

	public static void addUniversal(Concept lhs, UniversalConcept rhs) {
		totalUniv++;
//		System.err.println(" universals : " + lhs+" => "+rhs);
		Role r = rhs.getRole();
		Map<Concept, Set<Concept>> umap = null;
		if (normalizedUniversals.containsKey(r)) {
			umap = normalizedUniversals.get(r);
		} else {
			umap = new HashMap<Concept, Set<Concept>>();
		}
		Concept filler = rhs.getFiller();
		if (umap.containsKey(lhs)) {
			umap.get(lhs).add(filler);
		} else {
			Set<Concept> cs = new HashSet<Concept>();
			cs.add(filler);
			umap.put(lhs, cs);
		}
		normalizedUniversals.put(r, umap);
	}



	protected static void optimizeUR(TBox tb)
			throws CoreReasoningException {
		if(!OptimizedRestrictions.OptimizeUR){
			return;
		}
		ExecTime timer = ExecTime.getStarted();
		// all Universal and RAs are collected
		for (Individual a : allRAs.keySet()) {
			Map<Role, HashSet<Individual>> rb = allRAs.get(a);
			for (Role r : rb.keySet()) {
				for (Individual b : rb.get(r)) {
					try {
						removeDefb(r, a, b, tb);
					} catch (AbsorptionException e) {
						e.printStackTrace();
					}
				}
			}
		}
		// end of all nested loops
//		long end = System.currentTimeMillis();
		if (verbose) {
			System.err.println("\n# of universals (A-> All R.B): " + totalUniv);
			System.err.println("# of guards removed (DEF_b) / hit /lookups : " + rmedDefs+"/"+realizedHit+"/"+lookup);
//			System.err.println("Replicated concept assertion: "+repData);
		}
		System.err.println("Optimization of local universals time: " + (timer.getTime()* 1.0 / 1000)+"\n");
	}

}
